The following is one simple example showing how to create a hashtable in C#.

using System.Collections; using PAT.Common.Classes.Expressions.ExpressionClass; //the namespace must be PAT.Lib, the class and method names can be arbitrary namespace PAT.Lib {     public class HashTable : ExpressionValue {         public Hashtable table;         /// Default constructor without any parameter must be implemented         public HashTable() {             table = new Hashtable();         }         public HashTable(Hashtable newTable) {             table = newTable;         }         public void Add(int key, int value) {             if(!table.ContainsKey(key)) {                 table.Add(key, value);             }         }                 public bool ContainsKey(int key) {             return table.ContainsKey(key);         }         public int GetValue(int key) {             return (int)table[key];         }         /// Return the string representation of the hash table.         /// This method must be overriden         public override string ToString() {             string returnString = "";             foreach (DictionaryEntry entry in table) {                 returnString += entry.Key + "=" + entry.Value + ",";             }             return returnString;         }   /// Return a deep clone of the hash table       /// NOTE: this must be a deep clone, shallow clone may lead to strange behaviors.         /// This method must be overriden         public override ExpressionValue GetClone() {             return new HashTable(new Hashtable(table));         }    /// Return the compact string representation of the hash table.         /// This method must be overriden         /// Smart implementation of this method can reduce the state space and speedup verification         public override string ExpressionID {            get {                string returnString = "";                      foreach (DictionaryEntry entry in table) {                             returnString += entry.Key + "=" + entry.Value + ",";                      }                return returnString;            }         } } }

Note the following requirements when you create your own data structure objects:

• The namespace must be "PAT.Lib", otherwise it will not be recognized. There is no restriction for class names and method names.
• Importing the PAT Expression name space using "using PAT.Common.Classes.Expressions.ExpressionClass;".
• Only public methods can be used in PAT models.
• The parameters must be of type "bool", "int", "int[]"  (int array) or object (object type allow user to pass user defined data type as parameter).
• Object type parameter are passed by reference, i.e., if the method changes the parameter values, the effect will stay in the PAT model.
• The number of parameters can be 0 or many.
• The return type must be of type "void", "bool", "int", "short", "byte", "int[]" (int array) or user defined data type.
• The method names are case sensitive.
• Put the compiled DLLs in "Lib" folder of the PAT installation directory to make the linking easy by using #import "DLL_Name";  or you can put the DLLs under same folder as the model. If the DLLs are put in other places, you need to put the full path of the DLLs after import keyword. 

If your methods need to handle exceptional cases, you can throw PAT runtime exceptions as illustrated as the following example.

public static int StackPeek(int[] array) {     if (array.Length > 0)            return array[array.Length - 1];     //throw PAT Runtime exception     throw new PAT.Common.Classes.Expressions.ExpressionClass.RuntimeException("Access an empty stack!"); }

To import the libraries in your model, users can using following syntax:

• #import "PAT.Lib.Hashtable"; //to import a library under Lib folder of PAT installation path
• #import "C:\Program Files\Intel\Hashtable.dll"; //to import a library using absolute path

To declare the user defined types in your models, please use the following syntax:

• var <HashTable> table; //use the class name here as the type of the variable.
• var <HashTable> table = new HashTable(4); //initialize the variable using the constructors provided.

To invoke the public methods in your models, please use the following syntax:

• table.Add(10, 2); //public method invocation
• if(table.ContainsKey(10))... //public method invocation with return values
• table$column //public field or property reading and writting

Note that there is no difference between user defined types and normal variables (e.g. var x =1;). Only when the process parameter is used as user defined types, it is user's responsibility to make sure that the correct variable type is passed in since most of PAT modules don't have explicit types. See the example below.

            #import "PAT.Lib.Set";
                  var<Set> set1;
                  Q() = P(set1);
                  P(i) = initialize{i.Add(1);}-> ([i.GetSize() > 0] Skip);

Warning:

When the user defined data variable (declared as global variable) is used in conditions (if-then-else/guard/while-loop), the operation should be side-effect free. One example is the guard expression "i.GetSize() > 0" Otherwise the verification results may not be correct.

           #import "PAT.Lib.Set";
                 var<Set> set1;
                 Q() = P(set1);
                 P(i) = add1{i.Add(1);} -> Skip [] add2{i.Add(2);} -> Skip;